abstract sig Person{
}

sig UnregisteredUser extends Person{
}

sig Ability{
}

sig User extends Person{
	abilities: set Ability
}

sig Friendship{
	users: set User,
	collaborations: set Collaboration
}{
	#users = 2
}

sig SimpleCollaboration{
	people: set Person
}{
	#people = 2
	#UnregisteredUser = 1
}

sig Collaboration extends SimpleCollaboration{
	users: set User,
	feedback: set Feedback
}{
	#users = 2
	#feedback < 3
}

sig Feedback{
	user: User
}{
	#user = 1
}

sig LightResearch{
	researcher: one Person,
	foundUsers: set User,
	abilities: some Ability
}

sig AdvancedResearch extends LightResearch{
}

/**
FRIENDSHIP FACTS
**/

fact noDoubleFriendship{	
//Two user can be two times friend
	all u1, u2: User | lone f: Friendship | u1 != u2 and u1 in f.users and u2 in f.users
}

/**
SIMPLE COLLABORATION, COLLABORATION and FEEDBACK FACTS
**/

fact noCollaborationWithoutFriendship{	
//Each collaboration is associated to one friendship, and they have same users
	all c:Collaboration | one f:Friendship | c in f.collaborations
	all c:Collaboration | c.users = c.people
	all c:Collaboration | one f:Friendship | c in f.collaborations and c.users  =  f.users
	all c:Collaboration | no f:Friendship | c.users  !=  f.users and c in f.collaborations
	
}

fact noFeedbackWithoutCollaboration{
//Each feedback is associated to one collaboration
	all f:Feedback | one c:Collaboration | f in c.feedback

//Each feedback is about a user in collaboration
	all f:Feedback | one c:Collaboration | f in c.feedback and f.user in c.users

//User has got just one feedback about one collaboration
	no u: User |
		some f1, f2: Feedback |
			some c: Collaboration |
				f1 != f2 and f1 in c.feedback and f2 in c.feedback and
				f1.user = u and f2.user  = u
}

/**
COLLABORATION and FEEDBACK ASSERTS
**/

//Two unregistered user can not have a collaboration in SWIM
assert noSimpleCollaborationBetweenTwoUU{
	no sc: SimpleCollaboration | sc.people in UnregisteredUser
}

check noSimpleCollaborationBetweenTwoUU for 10

//All feedbacks have got one friendship associated
assert noFeedbackWithoutFriendship{
	all fe:Feedback | one fr: Friendship | one c:Collaboration |
		fe.user in c.users and
		fe.user in fr.users and
		fe in c.feedback	and
		c.users = fr.users
}

check noFeedbackWithoutFriendship for 10

//No multiple feedback for one user in one collaboration
assert noMultipleFeedback{
	no f1, f2: Feedback | some c:Collaboration |
		f1 != f2 and
		f1.user = f2.user and
		f1 in c.feedback and f2 in c.feedback
}

check noMultipleFeedback for 10

/**
COLLABORATION PREDICATE
**/

//Show an interesting case of collaboration
pred showCollaboration(){
	#Collaboration>0
	#SimpleCollaboration > 0
	#Feedback>0
	some sc: SimpleCollaboration| one uu:UnregisteredUser | uu in sc.people
	some c:Collaboration | #c.feedback>1
}

run showCollaboration for 5

/**
LIGHTRESEARCH and ADVANCEDRESEARCH FACTS
**/

fact usersInLightResearch{
//Each user in found user has all searched abilties
	no lr: LightResearch | some u:User | !(lr.abilities in u.abilities) and u in lr.foundUsers

//Every users in SWIM system that match research are in found users of Light Research
	no u: User |
		some lr: LightResearch |
			!(u in lr.researcher) and !(u in lr.foundUsers) 
			and lr.abilities in u.abilities

//A user can't find himself
	no lr: LightResearch | lr.researcher in lr.foundUsers

}

//Advanced research can be done just by user, not by an unregistered user
fact advancedResearchJustForUsers{
	all ar: AdvancedResearch | no uu: UnregisteredUser | uu = ar.researcher
}

/**
LIGHTRESEARCH ASSERT
**/

//All found users have all searched abilities
assert allFoundUserHaveSearchedAbilities{
	no u:User | some lr:LightResearch | some a: Ability |
		u in lr.foundUsers and
		a in lr.abilities and
		!(a in u.abilities)
}

check allFoundUserHaveSearchedAbilities for 10

/**
RESEARCH PREDICATE
**/

//Show an interesing case of light and advanced research
pred showResearch{
	#User > 2
	#Ability >1
	some lr: LightResearch | some uu: UnregisteredUser |
		lr.researcher = uu
	some lr: LightResearch |
		some a:Ability |
			some u:User |
				lr.researcher = u and a in u.abilities and a in lr.abilities and #lr.foundUsers > 0
}

run showResearch for 5 but 2 LightResearch, 1 AdvancedResearch, 0 SimpleCollaboration,
0 Friendship
